The Runtime Complexity (innermost) of the given CpxTRS could be proven to be BOUNDS(O(1), O(n^1)).

0 CpxTRS
↳1 CpxTrsToCdtProof (BOTH BOUNDS(ID, ID), 88 ms)
↳2 CdtProblem
    ↳3 CdtLeafRemovalProof (BOTH BOUNDS(ID, ID), 0 ms)
    ↳4 CdtProblem
    ↳5 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))), 487 ms)
    ↳6 CdtProblem
    ↳7 CdtNarrowingProof (BOTH BOUNDS(ID, ID), 0 ms)
    ↳8 CdtProblem
    ↳9 CdtLeafRemovalProof (BOTH BOUNDS(ID, ID), 0 ms)
    ↳10 CdtProblem
    ↳11 CdtNarrowingProof (BOTH BOUNDS(ID, ID), 5 ms)
    ↳12 CdtProblem
    ↳13 CdtLeafRemovalProof (BOTH BOUNDS(ID, ID), 0 ms)
    ↳14 CdtProblem
    ↳15 CdtNarrowingProof (BOTH BOUNDS(ID, ID), 0 ms)
    ↳16 CdtProblem
    ↳17 CdtLeafRemovalProof (BOTH BOUNDS(ID, ID), 0 ms)
    ↳18 CdtProblem
    ↳19 CdtNarrowingProof (BOTH BOUNDS(ID, ID), 0 ms)
    ↳20 CdtProblem
    ↳21 CdtLeafRemovalProof (BOTH BOUNDS(ID, ID), 0 ms)
    ↳22 CdtProblem
    ↳23 CdtNarrowingProof (BOTH BOUNDS(ID, ID), 0 ms)
    ↳24 CdtProblem
    ↳25 CdtLeafRemovalProof (BOTH BOUNDS(ID, ID), 0 ms)
    ↳26 CdtProblem
    ↳27 CdtNarrowingProof (BOTH BOUNDS(ID, ID), 0 ms)
    ↳28 CdtProblem
    ↳29 CdtNarrowingProof (BOTH BOUNDS(ID, ID), 0 ms)
    ↳30 CdtProblem
↳31 CpxTrsMatchBoundsTAProof (⇔, 0 ms)
↳32 BOUNDS(O(1), O(n^1))

(0) Obligation:

Runtime Complexity TRS:
The TRS R consists of the following rules:

+(p1, p1) → p2
+(p1, +(p2, p2)) → p5
+(p5, p5) → p10
+(+(x, y), z) → +(x, +(y, z))
+(p1, +(p1, x)) → +(p2, x)
+(p1, +(p2, +(p2, x))) → +(p5, x)
+(p2, p1) → +(p1, p2)
+(p2, +(p1, x)) → +(p1, +(p2, x))
+(p2, +(p2, p2)) → +(p1, p5)
+(p2, +(p2, +(p2, x))) → +(p1, +(p5, x))
+(p5, p1) → +(p1, p5)
+(p5, +(p1, x)) → +(p1, +(p5, x))
+(p5, p2) → +(p2, p5)
+(p5, +(p2, x)) → +(p2, +(p5, x))
+(p5, +(p5, x)) → +(p10, x)
+(p10, p1) → +(p1, p10)
+(p10, +(p1, x)) → +(p1, +(p10, x))
+(p10, p2) → +(p2, p10)
+(p10, +(p2, x)) → +(p2, +(p10, x))
+(p10, p5) → +(p5, p10)
+(p10, +(p5, x)) → +(p5, +(p10, x))

Rewrite Strategy: INNERMOST

(1) CpxTrsToCdtProof (BOTH BOUNDS(ID, ID) transformation)

Converted CpxTRS to CDT

(2) Obligation:

Complexity Dependency Tuples Problem
Rules:

+(p1, p1) → p2
+(p1, +(p2, p2)) → p5
+(p5, p5) → p10
+(+(z0, z1), z2) → +(z0, +(z1, z2))
+(p1, +(p1, z0)) → +(p2, z0)
+(p1, +(p2, +(p2, z0))) → +(p5, z0)
+(p2, p1) → +(p1, p2)
+(p2, +(p1, z0)) → +(p1, +(p2, z0))
+(p2, +(p2, p2)) → +(p1, p5)
+(p2, +(p2, +(p2, z0))) → +(p1, +(p5, z0))
+(p5, p1) → +(p1, p5)
+(p5, +(p1, z0)) → +(p1, +(p5, z0))
+(p5, p2) → +(p2, p5)
+(p5, +(p2, z0)) → +(p2, +(p5, z0))
+(p5, +(p5, z0)) → +(p10, z0)
+(p10, p1) → +(p1, p10)
+(p10, +(p1, z0)) → +(p1, +(p10, z0))
+(p10, p2) → +(p2, p10)
+(p10, +(p2, z0)) → +(p2, +(p10, z0))
+(p10, p5) → +(p5, p10)
+(p10, +(p5, z0)) → +(p5, +(p10, z0))
Tuples:

+'(+(z0, z1), z2) → c3(+'(z0, +(z1, z2)), +'(z1, z2))
+'(p1, +(p1, z0)) → c4(+'(p2, z0))
+'(p1, +(p2, +(p2, z0))) → c5(+'(p5, z0))
+'(p2, p1) → c6(+'(p1, p2))
+'(p2, +(p1, z0)) → c7(+'(p1, +(p2, z0)), +'(p2, z0))
+'(p2, +(p2, p2)) → c8(+'(p1, p5))
+'(p2, +(p2, +(p2, z0))) → c9(+'(p1, +(p5, z0)), +'(p5, z0))
+'(p5, p1) → c10(+'(p1, p5))
+'(p5, +(p1, z0)) → c11(+'(p1, +(p5, z0)), +'(p5, z0))
+'(p5, p2) → c12(+'(p2, p5))
+'(p5, +(p2, z0)) → c13(+'(p2, +(p5, z0)), +'(p5, z0))
+'(p5, +(p5, z0)) → c14(+'(p10, z0))
+'(p10, p1) → c15(+'(p1, p10))
+'(p10, +(p1, z0)) → c16(+'(p1, +(p10, z0)), +'(p10, z0))
+'(p10, p2) → c17(+'(p2, p10))
+'(p10, +(p2, z0)) → c18(+'(p2, +(p10, z0)), +'(p10, z0))
+'(p10, p5) → c19(+'(p5, p10))
+'(p10, +(p5, z0)) → c20(+'(p5, +(p10, z0)), +'(p10, z0))
S tuples:

+'(+(z0, z1), z2) → c3(+'(z0, +(z1, z2)), +'(z1, z2))
+'(p1, +(p1, z0)) → c4(+'(p2, z0))
+'(p1, +(p2, +(p2, z0))) → c5(+'(p5, z0))
+'(p2, p1) → c6(+'(p1, p2))
+'(p2, +(p1, z0)) → c7(+'(p1, +(p2, z0)), +'(p2, z0))
+'(p2, +(p2, p2)) → c8(+'(p1, p5))
+'(p2, +(p2, +(p2, z0))) → c9(+'(p1, +(p5, z0)), +'(p5, z0))
+'(p5, p1) → c10(+'(p1, p5))
+'(p5, +(p1, z0)) → c11(+'(p1, +(p5, z0)), +'(p5, z0))
+'(p5, p2) → c12(+'(p2, p5))
+'(p5, +(p2, z0)) → c13(+'(p2, +(p5, z0)), +'(p5, z0))
+'(p5, +(p5, z0)) → c14(+'(p10, z0))
+'(p10, p1) → c15(+'(p1, p10))
+'(p10, +(p1, z0)) → c16(+'(p1, +(p10, z0)), +'(p10, z0))
+'(p10, p2) → c17(+'(p2, p10))
+'(p10, +(p2, z0)) → c18(+'(p2, +(p10, z0)), +'(p10, z0))
+'(p10, p5) → c19(+'(p5, p10))
+'(p10, +(p5, z0)) → c20(+'(p5, +(p10, z0)), +'(p10, z0))
K tuples:none
Defined Rule Symbols:

+

Defined Pair Symbols:

+'

Compound Symbols:

c3, c4, c5, c6, c7, c8, c9, c10, c11, c12, c13, c14, c15, c16, c17, c18, c19, c20

(3) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID) transformation)

Removed 7 trailing nodes:

+'(p10, p5) → c19(+'(p5, p10))
+'(p2, +(p2, p2)) → c8(+'(p1, p5))
+'(p10, p2) → c17(+'(p2, p10))
+'(p5, p1) → c10(+'(p1, p5))
+'(p2, p1) → c6(+'(p1, p2))
+'(p10, p1) → c15(+'(p1, p10))
+'(p5, p2) → c12(+'(p2, p5))

(4) Obligation:

Complexity Dependency Tuples Problem
Rules:

+(p1, p1) → p2
+(p1, +(p2, p2)) → p5
+(p5, p5) → p10
+(+(z0, z1), z2) → +(z0, +(z1, z2))
+(p1, +(p1, z0)) → +(p2, z0)
+(p1, +(p2, +(p2, z0))) → +(p5, z0)
+(p2, p1) → +(p1, p2)
+(p2, +(p1, z0)) → +(p1, +(p2, z0))
+(p2, +(p2, p2)) → +(p1, p5)
+(p2, +(p2, +(p2, z0))) → +(p1, +(p5, z0))
+(p5, p1) → +(p1, p5)
+(p5, +(p1, z0)) → +(p1, +(p5, z0))
+(p5, p2) → +(p2, p5)
+(p5, +(p2, z0)) → +(p2, +(p5, z0))
+(p5, +(p5, z0)) → +(p10, z0)
+(p10, p1) → +(p1, p10)
+(p10, +(p1, z0)) → +(p1, +(p10, z0))
+(p10, p2) → +(p2, p10)
+(p10, +(p2, z0)) → +(p2, +(p10, z0))
+(p10, p5) → +(p5, p10)
+(p10, +(p5, z0)) → +(p5, +(p10, z0))
Tuples:

+'(+(z0, z1), z2) → c3(+'(z0, +(z1, z2)), +'(z1, z2))
+'(p1, +(p1, z0)) → c4(+'(p2, z0))
+'(p1, +(p2, +(p2, z0))) → c5(+'(p5, z0))
+'(p2, +(p1, z0)) → c7(+'(p1, +(p2, z0)), +'(p2, z0))
+'(p2, +(p2, +(p2, z0))) → c9(+'(p1, +(p5, z0)), +'(p5, z0))
+'(p5, +(p1, z0)) → c11(+'(p1, +(p5, z0)), +'(p5, z0))
+'(p5, +(p2, z0)) → c13(+'(p2, +(p5, z0)), +'(p5, z0))
+'(p5, +(p5, z0)) → c14(+'(p10, z0))
+'(p10, +(p1, z0)) → c16(+'(p1, +(p10, z0)), +'(p10, z0))
+'(p10, +(p2, z0)) → c18(+'(p2, +(p10, z0)), +'(p10, z0))
+'(p10, +(p5, z0)) → c20(+'(p5, +(p10, z0)), +'(p10, z0))
S tuples:

+'(+(z0, z1), z2) → c3(+'(z0, +(z1, z2)), +'(z1, z2))
+'(p1, +(p1, z0)) → c4(+'(p2, z0))
+'(p1, +(p2, +(p2, z0))) → c5(+'(p5, z0))
+'(p2, +(p1, z0)) → c7(+'(p1, +(p2, z0)), +'(p2, z0))
+'(p2, +(p2, +(p2, z0))) → c9(+'(p1, +(p5, z0)), +'(p5, z0))
+'(p5, +(p1, z0)) → c11(+'(p1, +(p5, z0)), +'(p5, z0))
+'(p5, +(p2, z0)) → c13(+'(p2, +(p5, z0)), +'(p5, z0))
+'(p5, +(p5, z0)) → c14(+'(p10, z0))
+'(p10, +(p1, z0)) → c16(+'(p1, +(p10, z0)), +'(p10, z0))
+'(p10, +(p2, z0)) → c18(+'(p2, +(p10, z0)), +'(p10, z0))
+'(p10, +(p5, z0)) → c20(+'(p5, +(p10, z0)), +'(p10, z0))
K tuples:none
Defined Rule Symbols:

+

Defined Pair Symbols:

+'

Compound Symbols:

c3, c4, c5, c7, c9, c11, c13, c14, c16, c18, c20

(5) CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))) transformation)

Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.

+'(+(z0, z1), z2) → c3(+'(z0, +(z1, z2)), +'(z1, z2))
We considered the (Usable) Rules:

+(p10, p2) → +(p2, p10)
+(p10, +(p2, z0)) → +(p2, +(p10, z0))
+(p10, p5) → +(p5, p10)
+(p10, +(p5, z0)) → +(p5, +(p10, z0))
+(p2, p1) → +(p1, p2)
+(p2, +(p1, z0)) → +(p1, +(p2, z0))
+(p2, +(p2, p2)) → +(p1, p5)
+(p2, +(p2, +(p2, z0))) → +(p1, +(p5, z0))
+(p5, p5) → p10
+(p5, +(p5, z0)) → +(p10, z0)
+(p1, p1) → p2
+(p1, +(p2, p2)) → p5
+(p1, +(p1, z0)) → +(p2, z0)
+(p1, +(p2, +(p2, z0))) → +(p5, z0)
+(p5, p2) → +(p2, p5)
+(p5, +(p2, z0)) → +(p2, +(p5, z0))
+(+(z0, z1), z2) → +(z0, +(z1, z2))
+(p5, p1) → +(p1, p5)
+(p5, +(p1, z0)) → +(p1, +(p5, z0))
+(p10, p1) → +(p1, p10)
+(p10, +(p1, z0)) → +(p1, +(p10, z0))
And the Tuples:

+'(+(z0, z1), z2) → c3(+'(z0, +(z1, z2)), +'(z1, z2))
+'(p1, +(p1, z0)) → c4(+'(p2, z0))
+'(p1, +(p2, +(p2, z0))) → c5(+'(p5, z0))
+'(p2, +(p1, z0)) → c7(+'(p1, +(p2, z0)), +'(p2, z0))
+'(p2, +(p2, +(p2, z0))) → c9(+'(p1, +(p5, z0)), +'(p5, z0))
+'(p5, +(p1, z0)) → c11(+'(p1, +(p5, z0)), +'(p5, z0))
+'(p5, +(p2, z0)) → c13(+'(p2, +(p5, z0)), +'(p5, z0))
+'(p5, +(p5, z0)) → c14(+'(p10, z0))
+'(p10, +(p1, z0)) → c16(+'(p1, +(p10, z0)), +'(p10, z0))
+'(p10, +(p2, z0)) → c18(+'(p2, +(p10, z0)), +'(p10, z0))
+'(p10, +(p5, z0)) → c20(+'(p5, +(p10, z0)), +'(p10, z0))
The order we found is given by the following interpretation:
Polynomial interpretation :

POL(+(x1, x2)) = [2] + [2]x1 + x2   
POL(+'(x1, x2)) = x1   
POL(c11(x1, x2)) = x1 + x2   
POL(c13(x1, x2)) = x1 + x2   
POL(c14(x1)) = x1   
POL(c16(x1, x2)) = x1 + x2   
POL(c18(x1, x2)) = x1 + x2   
POL(c20(x1, x2)) = x1 + x2   
POL(c3(x1, x2)) = x1 + x2   
POL(c4(x1)) = x1   
POL(c5(x1)) = x1   
POL(c7(x1, x2)) = x1 + x2   
POL(c9(x1, x2)) = x1 + x2   
POL(p1) = 0   
POL(p10) = 0   
POL(p2) = 0   
POL(p5) = 0   

(6) Obligation:

Complexity Dependency Tuples Problem
Rules:

+(p1, p1) → p2
+(p1, +(p2, p2)) → p5
+(p5, p5) → p10
+(+(z0, z1), z2) → +(z0, +(z1, z2))
+(p1, +(p1, z0)) → +(p2, z0)
+(p1, +(p2, +(p2, z0))) → +(p5, z0)
+(p2, p1) → +(p1, p2)
+(p2, +(p1, z0)) → +(p1, +(p2, z0))
+(p2, +(p2, p2)) → +(p1, p5)
+(p2, +(p2, +(p2, z0))) → +(p1, +(p5, z0))
+(p5, p1) → +(p1, p5)
+(p5, +(p1, z0)) → +(p1, +(p5, z0))
+(p5, p2) → +(p2, p5)
+(p5, +(p2, z0)) → +(p2, +(p5, z0))
+(p5, +(p5, z0)) → +(p10, z0)
+(p10, p1) → +(p1, p10)
+(p10, +(p1, z0)) → +(p1, +(p10, z0))
+(p10, p2) → +(p2, p10)
+(p10, +(p2, z0)) → +(p2, +(p10, z0))
+(p10, p5) → +(p5, p10)
+(p10, +(p5, z0)) → +(p5, +(p10, z0))
Tuples:

+'(+(z0, z1), z2) → c3(+'(z0, +(z1, z2)), +'(z1, z2))
+'(p1, +(p1, z0)) → c4(+'(p2, z0))
+'(p1, +(p2, +(p2, z0))) → c5(+'(p5, z0))
+'(p2, +(p1, z0)) → c7(+'(p1, +(p2, z0)), +'(p2, z0))
+'(p2, +(p2, +(p2, z0))) → c9(+'(p1, +(p5, z0)), +'(p5, z0))
+'(p5, +(p1, z0)) → c11(+'(p1, +(p5, z0)), +'(p5, z0))
+'(p5, +(p2, z0)) → c13(+'(p2, +(p5, z0)), +'(p5, z0))
+'(p5, +(p5, z0)) → c14(+'(p10, z0))
+'(p10, +(p1, z0)) → c16(+'(p1, +(p10, z0)), +'(p10, z0))
+'(p10, +(p2, z0)) → c18(+'(p2, +(p10, z0)), +'(p10, z0))
+'(p10, +(p5, z0)) → c20(+'(p5, +(p10, z0)), +'(p10, z0))
S tuples:

+'(p1, +(p1, z0)) → c4(+'(p2, z0))
+'(p1, +(p2, +(p2, z0))) → c5(+'(p5, z0))
+'(p2, +(p1, z0)) → c7(+'(p1, +(p2, z0)), +'(p2, z0))
+'(p2, +(p2, +(p2, z0))) → c9(+'(p1, +(p5, z0)), +'(p5, z0))
+'(p5, +(p1, z0)) → c11(+'(p1, +(p5, z0)), +'(p5, z0))
+'(p5, +(p2, z0)) → c13(+'(p2, +(p5, z0)), +'(p5, z0))
+'(p5, +(p5, z0)) → c14(+'(p10, z0))
+'(p10, +(p1, z0)) → c16(+'(p1, +(p10, z0)), +'(p10, z0))
+'(p10, +(p2, z0)) → c18(+'(p2, +(p10, z0)), +'(p10, z0))
+'(p10, +(p5, z0)) → c20(+'(p5, +(p10, z0)), +'(p10, z0))
K tuples:

+'(+(z0, z1), z2) → c3(+'(z0, +(z1, z2)), +'(z1, z2))
Defined Rule Symbols:

+

Defined Pair Symbols:

+'

Compound Symbols:

c3, c4, c5, c7, c9, c11, c13, c14, c16, c18, c20

(7) CdtNarrowingProof (BOTH BOUNDS(ID, ID) transformation)

Use narrowing to replace +'(p2, +(p2, +(p2, z0))) → c9(+'(p1, +(p5, z0)), +'(p5, z0)) by

+'(p2, +(p2, +(p2, p5))) → c9(+'(p1, p10), +'(p5, p5))
+'(p2, +(p2, +(p2, +(p5, z0)))) → c9(+'(p1, +(p10, z0)), +'(p5, +(p5, z0)))
+'(p2, +(p2, +(p2, x0))) → c9(+'(p5, x0))

(8) Obligation:

Complexity Dependency Tuples Problem
Rules:

+(p1, p1) → p2
+(p1, +(p2, p2)) → p5
+(p5, p5) → p10
+(+(z0, z1), z2) → +(z0, +(z1, z2))
+(p1, +(p1, z0)) → +(p2, z0)
+(p1, +(p2, +(p2, z0))) → +(p5, z0)
+(p2, p1) → +(p1, p2)
+(p2, +(p1, z0)) → +(p1, +(p2, z0))
+(p2, +(p2, p2)) → +(p1, p5)
+(p2, +(p2, +(p2, z0))) → +(p1, +(p5, z0))
+(p5, p1) → +(p1, p5)
+(p5, +(p1, z0)) → +(p1, +(p5, z0))
+(p5, p2) → +(p2, p5)
+(p5, +(p2, z0)) → +(p2, +(p5, z0))
+(p5, +(p5, z0)) → +(p10, z0)
+(p10, p1) → +(p1, p10)
+(p10, +(p1, z0)) → +(p1, +(p10, z0))
+(p10, p2) → +(p2, p10)
+(p10, +(p2, z0)) → +(p2, +(p10, z0))
+(p10, p5) → +(p5, p10)
+(p10, +(p5, z0)) → +(p5, +(p10, z0))
Tuples:

+'(+(z0, z1), z2) → c3(+'(z0, +(z1, z2)), +'(z1, z2))
+'(p1, +(p1, z0)) → c4(+'(p2, z0))
+'(p1, +(p2, +(p2, z0))) → c5(+'(p5, z0))
+'(p2, +(p1, z0)) → c7(+'(p1, +(p2, z0)), +'(p2, z0))
+'(p5, +(p1, z0)) → c11(+'(p1, +(p5, z0)), +'(p5, z0))
+'(p5, +(p2, z0)) → c13(+'(p2, +(p5, z0)), +'(p5, z0))
+'(p5, +(p5, z0)) → c14(+'(p10, z0))
+'(p10, +(p1, z0)) → c16(+'(p1, +(p10, z0)), +'(p10, z0))
+'(p10, +(p2, z0)) → c18(+'(p2, +(p10, z0)), +'(p10, z0))
+'(p10, +(p5, z0)) → c20(+'(p5, +(p10, z0)), +'(p10, z0))
+'(p2, +(p2, +(p2, p5))) → c9(+'(p1, p10), +'(p5, p5))
+'(p2, +(p2, +(p2, +(p5, z0)))) → c9(+'(p1, +(p10, z0)), +'(p5, +(p5, z0)))
+'(p2, +(p2, +(p2, x0))) → c9(+'(p5, x0))
S tuples:

+'(p1, +(p1, z0)) → c4(+'(p2, z0))
+'(p1, +(p2, +(p2, z0))) → c5(+'(p5, z0))
+'(p2, +(p1, z0)) → c7(+'(p1, +(p2, z0)), +'(p2, z0))
+'(p5, +(p1, z0)) → c11(+'(p1, +(p5, z0)), +'(p5, z0))
+'(p5, +(p2, z0)) → c13(+'(p2, +(p5, z0)), +'(p5, z0))
+'(p5, +(p5, z0)) → c14(+'(p10, z0))
+'(p10, +(p1, z0)) → c16(+'(p1, +(p10, z0)), +'(p10, z0))
+'(p10, +(p2, z0)) → c18(+'(p2, +(p10, z0)), +'(p10, z0))
+'(p10, +(p5, z0)) → c20(+'(p5, +(p10, z0)), +'(p10, z0))
+'(p2, +(p2, +(p2, p5))) → c9(+'(p1, p10), +'(p5, p5))
+'(p2, +(p2, +(p2, +(p5, z0)))) → c9(+'(p1, +(p10, z0)), +'(p5, +(p5, z0)))
+'(p2, +(p2, +(p2, x0))) → c9(+'(p5, x0))
K tuples:

+'(+(z0, z1), z2) → c3(+'(z0, +(z1, z2)), +'(z1, z2))
Defined Rule Symbols:

+

Defined Pair Symbols:

+'

Compound Symbols:

c3, c4, c5, c7, c11, c13, c14, c16, c18, c20, c9, c9

(9) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID) transformation)

Removed 1 trailing nodes:

+'(p2, +(p2, +(p2, p5))) → c9(+'(p1, p10), +'(p5, p5))

(10) Obligation:

Complexity Dependency Tuples Problem
Rules:

+(p1, p1) → p2
+(p1, +(p2, p2)) → p5
+(p5, p5) → p10
+(+(z0, z1), z2) → +(z0, +(z1, z2))
+(p1, +(p1, z0)) → +(p2, z0)
+(p1, +(p2, +(p2, z0))) → +(p5, z0)
+(p2, p1) → +(p1, p2)
+(p2, +(p1, z0)) → +(p1, +(p2, z0))
+(p2, +(p2, p2)) → +(p1, p5)
+(p2, +(p2, +(p2, z0))) → +(p1, +(p5, z0))
+(p5, p1) → +(p1, p5)
+(p5, +(p1, z0)) → +(p1, +(p5, z0))
+(p5, p2) → +(p2, p5)
+(p5, +(p2, z0)) → +(p2, +(p5, z0))
+(p5, +(p5, z0)) → +(p10, z0)
+(p10, p1) → +(p1, p10)
+(p10, +(p1, z0)) → +(p1, +(p10, z0))
+(p10, p2) → +(p2, p10)
+(p10, +(p2, z0)) → +(p2, +(p10, z0))
+(p10, p5) → +(p5, p10)
+(p10, +(p5, z0)) → +(p5, +(p10, z0))
Tuples:

+'(+(z0, z1), z2) → c3(+'(z0, +(z1, z2)), +'(z1, z2))
+'(p1, +(p1, z0)) → c4(+'(p2, z0))
+'(p1, +(p2, +(p2, z0))) → c5(+'(p5, z0))
+'(p2, +(p1, z0)) → c7(+'(p1, +(p2, z0)), +'(p2, z0))
+'(p5, +(p1, z0)) → c11(+'(p1, +(p5, z0)), +'(p5, z0))
+'(p5, +(p2, z0)) → c13(+'(p2, +(p5, z0)), +'(p5, z0))
+'(p5, +(p5, z0)) → c14(+'(p10, z0))
+'(p10, +(p1, z0)) → c16(+'(p1, +(p10, z0)), +'(p10, z0))
+'(p10, +(p2, z0)) → c18(+'(p2, +(p10, z0)), +'(p10, z0))
+'(p10, +(p5, z0)) → c20(+'(p5, +(p10, z0)), +'(p10, z0))
+'(p2, +(p2, +(p2, +(p5, z0)))) → c9(+'(p1, +(p10, z0)), +'(p5, +(p5, z0)))
+'(p2, +(p2, +(p2, x0))) → c9(+'(p5, x0))
S tuples:

+'(p1, +(p1, z0)) → c4(+'(p2, z0))
+'(p1, +(p2, +(p2, z0))) → c5(+'(p5, z0))
+'(p2, +(p1, z0)) → c7(+'(p1, +(p2, z0)), +'(p2, z0))
+'(p5, +(p1, z0)) → c11(+'(p1, +(p5, z0)), +'(p5, z0))
+'(p5, +(p2, z0)) → c13(+'(p2, +(p5, z0)), +'(p5, z0))
+'(p5, +(p5, z0)) → c14(+'(p10, z0))
+'(p10, +(p1, z0)) → c16(+'(p1, +(p10, z0)), +'(p10, z0))
+'(p10, +(p2, z0)) → c18(+'(p2, +(p10, z0)), +'(p10, z0))
+'(p10, +(p5, z0)) → c20(+'(p5, +(p10, z0)), +'(p10, z0))
+'(p2, +(p2, +(p2, +(p5, z0)))) → c9(+'(p1, +(p10, z0)), +'(p5, +(p5, z0)))
+'(p2, +(p2, +(p2, x0))) → c9(+'(p5, x0))
K tuples:

+'(+(z0, z1), z2) → c3(+'(z0, +(z1, z2)), +'(z1, z2))
Defined Rule Symbols:

+

Defined Pair Symbols:

+'

Compound Symbols:

c3, c4, c5, c7, c11, c13, c14, c16, c18, c20, c9, c9

(11) CdtNarrowingProof (BOTH BOUNDS(ID, ID) transformation)

Use narrowing to replace +'(p5, +(p1, z0)) → c11(+'(p1, +(p5, z0)), +'(p5, z0)) by

+'(p5, +(p1, p5)) → c11(+'(p1, p10), +'(p5, p5))
+'(p5, +(p1, p2)) → c11(+'(p1, +(p2, p5)), +'(p5, p2))
+'(p5, +(p1, +(p2, z0))) → c11(+'(p1, +(p2, +(p5, z0))), +'(p5, +(p2, z0)))
+'(p5, +(p1, +(p5, z0))) → c11(+'(p1, +(p10, z0)), +'(p5, +(p5, z0)))
+'(p5, +(p1, x0)) → c11(+'(p5, x0))

(12) Obligation:

Complexity Dependency Tuples Problem
Rules:

+(p1, p1) → p2
+(p1, +(p2, p2)) → p5
+(p5, p5) → p10
+(+(z0, z1), z2) → +(z0, +(z1, z2))
+(p1, +(p1, z0)) → +(p2, z0)
+(p1, +(p2, +(p2, z0))) → +(p5, z0)
+(p2, p1) → +(p1, p2)
+(p2, +(p1, z0)) → +(p1, +(p2, z0))
+(p2, +(p2, p2)) → +(p1, p5)
+(p2, +(p2, +(p2, z0))) → +(p1, +(p5, z0))
+(p5, p1) → +(p1, p5)
+(p5, +(p1, z0)) → +(p1, +(p5, z0))
+(p5, p2) → +(p2, p5)
+(p5, +(p2, z0)) → +(p2, +(p5, z0))
+(p5, +(p5, z0)) → +(p10, z0)
+(p10, p1) → +(p1, p10)
+(p10, +(p1, z0)) → +(p1, +(p10, z0))
+(p10, p2) → +(p2, p10)
+(p10, +(p2, z0)) → +(p2, +(p10, z0))
+(p10, p5) → +(p5, p10)
+(p10, +(p5, z0)) → +(p5, +(p10, z0))
Tuples:

+'(+(z0, z1), z2) → c3(+'(z0, +(z1, z2)), +'(z1, z2))
+'(p1, +(p1, z0)) → c4(+'(p2, z0))
+'(p1, +(p2, +(p2, z0))) → c5(+'(p5, z0))
+'(p2, +(p1, z0)) → c7(+'(p1, +(p2, z0)), +'(p2, z0))
+'(p5, +(p2, z0)) → c13(+'(p2, +(p5, z0)), +'(p5, z0))
+'(p5, +(p5, z0)) → c14(+'(p10, z0))
+'(p10, +(p1, z0)) → c16(+'(p1, +(p10, z0)), +'(p10, z0))
+'(p10, +(p2, z0)) → c18(+'(p2, +(p10, z0)), +'(p10, z0))
+'(p10, +(p5, z0)) → c20(+'(p5, +(p10, z0)), +'(p10, z0))
+'(p2, +(p2, +(p2, +(p5, z0)))) → c9(+'(p1, +(p10, z0)), +'(p5, +(p5, z0)))
+'(p2, +(p2, +(p2, x0))) → c9(+'(p5, x0))
+'(p5, +(p1, p5)) → c11(+'(p1, p10), +'(p5, p5))
+'(p5, +(p1, p2)) → c11(+'(p1, +(p2, p5)), +'(p5, p2))
+'(p5, +(p1, +(p2, z0))) → c11(+'(p1, +(p2, +(p5, z0))), +'(p5, +(p2, z0)))
+'(p5, +(p1, +(p5, z0))) → c11(+'(p1, +(p10, z0)), +'(p5, +(p5, z0)))
+'(p5, +(p1, x0)) → c11(+'(p5, x0))
S tuples:

+'(p1, +(p1, z0)) → c4(+'(p2, z0))
+'(p1, +(p2, +(p2, z0))) → c5(+'(p5, z0))
+'(p2, +(p1, z0)) → c7(+'(p1, +(p2, z0)), +'(p2, z0))
+'(p5, +(p2, z0)) → c13(+'(p2, +(p5, z0)), +'(p5, z0))
+'(p5, +(p5, z0)) → c14(+'(p10, z0))
+'(p10, +(p1, z0)) → c16(+'(p1, +(p10, z0)), +'(p10, z0))
+'(p10, +(p2, z0)) → c18(+'(p2, +(p10, z0)), +'(p10, z0))
+'(p10, +(p5, z0)) → c20(+'(p5, +(p10, z0)), +'(p10, z0))
+'(p2, +(p2, +(p2, +(p5, z0)))) → c9(+'(p1, +(p10, z0)), +'(p5, +(p5, z0)))
+'(p2, +(p2, +(p2, x0))) → c9(+'(p5, x0))
+'(p5, +(p1, p5)) → c11(+'(p1, p10), +'(p5, p5))
+'(p5, +(p1, p2)) → c11(+'(p1, +(p2, p5)), +'(p5, p2))
+'(p5, +(p1, +(p2, z0))) → c11(+'(p1, +(p2, +(p5, z0))), +'(p5, +(p2, z0)))
+'(p5, +(p1, +(p5, z0))) → c11(+'(p1, +(p10, z0)), +'(p5, +(p5, z0)))
+'(p5, +(p1, x0)) → c11(+'(p5, x0))
K tuples:

+'(+(z0, z1), z2) → c3(+'(z0, +(z1, z2)), +'(z1, z2))
Defined Rule Symbols:

+

Defined Pair Symbols:

+'

Compound Symbols:

c3, c4, c5, c7, c13, c14, c16, c18, c20, c9, c9, c11, c11

(13) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID) transformation)

Removed 2 trailing nodes:

+'(p5, +(p1, p5)) → c11(+'(p1, p10), +'(p5, p5))
+'(p5, +(p1, p2)) → c11(+'(p1, +(p2, p5)), +'(p5, p2))

(14) Obligation:

Complexity Dependency Tuples Problem
Rules:

+(p1, p1) → p2
+(p1, +(p2, p2)) → p5
+(p5, p5) → p10
+(+(z0, z1), z2) → +(z0, +(z1, z2))
+(p1, +(p1, z0)) → +(p2, z0)
+(p1, +(p2, +(p2, z0))) → +(p5, z0)
+(p2, p1) → +(p1, p2)
+(p2, +(p1, z0)) → +(p1, +(p2, z0))
+(p2, +(p2, p2)) → +(p1, p5)
+(p2, +(p2, +(p2, z0))) → +(p1, +(p5, z0))
+(p5, p1) → +(p1, p5)
+(p5, +(p1, z0)) → +(p1, +(p5, z0))
+(p5, p2) → +(p2, p5)
+(p5, +(p2, z0)) → +(p2, +(p5, z0))
+(p5, +(p5, z0)) → +(p10, z0)
+(p10, p1) → +(p1, p10)
+(p10, +(p1, z0)) → +(p1, +(p10, z0))
+(p10, p2) → +(p2, p10)
+(p10, +(p2, z0)) → +(p2, +(p10, z0))
+(p10, p5) → +(p5, p10)
+(p10, +(p5, z0)) → +(p5, +(p10, z0))
Tuples:

+'(+(z0, z1), z2) → c3(+'(z0, +(z1, z2)), +'(z1, z2))
+'(p1, +(p1, z0)) → c4(+'(p2, z0))
+'(p1, +(p2, +(p2, z0))) → c5(+'(p5, z0))
+'(p2, +(p1, z0)) → c7(+'(p1, +(p2, z0)), +'(p2, z0))
+'(p5, +(p2, z0)) → c13(+'(p2, +(p5, z0)), +'(p5, z0))
+'(p5, +(p5, z0)) → c14(+'(p10, z0))
+'(p10, +(p1, z0)) → c16(+'(p1, +(p10, z0)), +'(p10, z0))
+'(p10, +(p2, z0)) → c18(+'(p2, +(p10, z0)), +'(p10, z0))
+'(p10, +(p5, z0)) → c20(+'(p5, +(p10, z0)), +'(p10, z0))
+'(p2, +(p2, +(p2, +(p5, z0)))) → c9(+'(p1, +(p10, z0)), +'(p5, +(p5, z0)))
+'(p2, +(p2, +(p2, x0))) → c9(+'(p5, x0))
+'(p5, +(p1, +(p2, z0))) → c11(+'(p1, +(p2, +(p5, z0))), +'(p5, +(p2, z0)))
+'(p5, +(p1, +(p5, z0))) → c11(+'(p1, +(p10, z0)), +'(p5, +(p5, z0)))
+'(p5, +(p1, x0)) → c11(+'(p5, x0))
S tuples:

+'(p1, +(p1, z0)) → c4(+'(p2, z0))
+'(p1, +(p2, +(p2, z0))) → c5(+'(p5, z0))
+'(p2, +(p1, z0)) → c7(+'(p1, +(p2, z0)), +'(p2, z0))
+'(p5, +(p2, z0)) → c13(+'(p2, +(p5, z0)), +'(p5, z0))
+'(p5, +(p5, z0)) → c14(+'(p10, z0))
+'(p10, +(p1, z0)) → c16(+'(p1, +(p10, z0)), +'(p10, z0))
+'(p10, +(p2, z0)) → c18(+'(p2, +(p10, z0)), +'(p10, z0))
+'(p10, +(p5, z0)) → c20(+'(p5, +(p10, z0)), +'(p10, z0))
+'(p2, +(p2, +(p2, +(p5, z0)))) → c9(+'(p1, +(p10, z0)), +'(p5, +(p5, z0)))
+'(p2, +(p2, +(p2, x0))) → c9(+'(p5, x0))
+'(p5, +(p1, +(p2, z0))) → c11(+'(p1, +(p2, +(p5, z0))), +'(p5, +(p2, z0)))
+'(p5, +(p1, +(p5, z0))) → c11(+'(p1, +(p10, z0)), +'(p5, +(p5, z0)))
+'(p5, +(p1, x0)) → c11(+'(p5, x0))
K tuples:

+'(+(z0, z1), z2) → c3(+'(z0, +(z1, z2)), +'(z1, z2))
Defined Rule Symbols:

+

Defined Pair Symbols:

+'

Compound Symbols:

c3, c4, c5, c7, c13, c14, c16, c18, c20, c9, c9, c11, c11

(15) CdtNarrowingProof (BOTH BOUNDS(ID, ID) transformation)

Use narrowing to replace +'(p5, +(p2, z0)) → c13(+'(p2, +(p5, z0)), +'(p5, z0)) by

+'(p5, +(p2, p5)) → c13(+'(p2, p10), +'(p5, p5))
+'(p5, +(p2, p2)) → c13(+'(p2, +(p2, p5)), +'(p5, p2))
+'(p5, +(p2, +(p2, z0))) → c13(+'(p2, +(p2, +(p5, z0))), +'(p5, +(p2, z0)))
+'(p5, +(p2, +(p5, z0))) → c13(+'(p2, +(p10, z0)), +'(p5, +(p5, z0)))
+'(p5, +(p2, x0)) → c13(+'(p5, x0))

(16) Obligation:

Complexity Dependency Tuples Problem
Rules:

+(p1, p1) → p2
+(p1, +(p2, p2)) → p5
+(p5, p5) → p10
+(+(z0, z1), z2) → +(z0, +(z1, z2))
+(p1, +(p1, z0)) → +(p2, z0)
+(p1, +(p2, +(p2, z0))) → +(p5, z0)
+(p2, p1) → +(p1, p2)
+(p2, +(p1, z0)) → +(p1, +(p2, z0))
+(p2, +(p2, p2)) → +(p1, p5)
+(p2, +(p2, +(p2, z0))) → +(p1, +(p5, z0))
+(p5, p1) → +(p1, p5)
+(p5, +(p1, z0)) → +(p1, +(p5, z0))
+(p5, p2) → +(p2, p5)
+(p5, +(p2, z0)) → +(p2, +(p5, z0))
+(p5, +(p5, z0)) → +(p10, z0)
+(p10, p1) → +(p1, p10)
+(p10, +(p1, z0)) → +(p1, +(p10, z0))
+(p10, p2) → +(p2, p10)
+(p10, +(p2, z0)) → +(p2, +(p10, z0))
+(p10, p5) → +(p5, p10)
+(p10, +(p5, z0)) → +(p5, +(p10, z0))
Tuples:

+'(+(z0, z1), z2) → c3(+'(z0, +(z1, z2)), +'(z1, z2))
+'(p1, +(p1, z0)) → c4(+'(p2, z0))
+'(p1, +(p2, +(p2, z0))) → c5(+'(p5, z0))
+'(p2, +(p1, z0)) → c7(+'(p1, +(p2, z0)), +'(p2, z0))
+'(p5, +(p5, z0)) → c14(+'(p10, z0))
+'(p10, +(p1, z0)) → c16(+'(p1, +(p10, z0)), +'(p10, z0))
+'(p10, +(p2, z0)) → c18(+'(p2, +(p10, z0)), +'(p10, z0))
+'(p10, +(p5, z0)) → c20(+'(p5, +(p10, z0)), +'(p10, z0))
+'(p2, +(p2, +(p2, +(p5, z0)))) → c9(+'(p1, +(p10, z0)), +'(p5, +(p5, z0)))
+'(p2, +(p2, +(p2, x0))) → c9(+'(p5, x0))
+'(p5, +(p1, +(p2, z0))) → c11(+'(p1, +(p2, +(p5, z0))), +'(p5, +(p2, z0)))
+'(p5, +(p1, +(p5, z0))) → c11(+'(p1, +(p10, z0)), +'(p5, +(p5, z0)))
+'(p5, +(p1, x0)) → c11(+'(p5, x0))
+'(p5, +(p2, p5)) → c13(+'(p2, p10), +'(p5, p5))
+'(p5, +(p2, p2)) → c13(+'(p2, +(p2, p5)), +'(p5, p2))
+'(p5, +(p2, +(p2, z0))) → c13(+'(p2, +(p2, +(p5, z0))), +'(p5, +(p2, z0)))
+'(p5, +(p2, +(p5, z0))) → c13(+'(p2, +(p10, z0)), +'(p5, +(p5, z0)))
+'(p5, +(p2, x0)) → c13(+'(p5, x0))
S tuples:

+'(p1, +(p1, z0)) → c4(+'(p2, z0))
+'(p1, +(p2, +(p2, z0))) → c5(+'(p5, z0))
+'(p2, +(p1, z0)) → c7(+'(p1, +(p2, z0)), +'(p2, z0))
+'(p5, +(p5, z0)) → c14(+'(p10, z0))
+'(p10, +(p1, z0)) → c16(+'(p1, +(p10, z0)), +'(p10, z0))
+'(p10, +(p2, z0)) → c18(+'(p2, +(p10, z0)), +'(p10, z0))
+'(p10, +(p5, z0)) → c20(+'(p5, +(p10, z0)), +'(p10, z0))
+'(p2, +(p2, +(p2, +(p5, z0)))) → c9(+'(p1, +(p10, z0)), +'(p5, +(p5, z0)))
+'(p2, +(p2, +(p2, x0))) → c9(+'(p5, x0))
+'(p5, +(p1, +(p2, z0))) → c11(+'(p1, +(p2, +(p5, z0))), +'(p5, +(p2, z0)))
+'(p5, +(p1, +(p5, z0))) → c11(+'(p1, +(p10, z0)), +'(p5, +(p5, z0)))
+'(p5, +(p1, x0)) → c11(+'(p5, x0))
+'(p5, +(p2, p5)) → c13(+'(p2, p10), +'(p5, p5))
+'(p5, +(p2, p2)) → c13(+'(p2, +(p2, p5)), +'(p5, p2))
+'(p5, +(p2, +(p2, z0))) → c13(+'(p2, +(p2, +(p5, z0))), +'(p5, +(p2, z0)))
+'(p5, +(p2, +(p5, z0))) → c13(+'(p2, +(p10, z0)), +'(p5, +(p5, z0)))
+'(p5, +(p2, x0)) → c13(+'(p5, x0))
K tuples:

+'(+(z0, z1), z2) → c3(+'(z0, +(z1, z2)), +'(z1, z2))
Defined Rule Symbols:

+

Defined Pair Symbols:

+'

Compound Symbols:

c3, c4, c5, c7, c14, c16, c18, c20, c9, c9, c11, c11, c13, c13

(17) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID) transformation)

Removed 2 trailing nodes:

+'(p5, +(p2, p5)) → c13(+'(p2, p10), +'(p5, p5))
+'(p5, +(p2, p2)) → c13(+'(p2, +(p2, p5)), +'(p5, p2))

(18) Obligation:

Complexity Dependency Tuples Problem
Rules:

+(p1, p1) → p2
+(p1, +(p2, p2)) → p5
+(p5, p5) → p10
+(+(z0, z1), z2) → +(z0, +(z1, z2))
+(p1, +(p1, z0)) → +(p2, z0)
+(p1, +(p2, +(p2, z0))) → +(p5, z0)
+(p2, p1) → +(p1, p2)
+(p2, +(p1, z0)) → +(p1, +(p2, z0))
+(p2, +(p2, p2)) → +(p1, p5)
+(p2, +(p2, +(p2, z0))) → +(p1, +(p5, z0))
+(p5, p1) → +(p1, p5)
+(p5, +(p1, z0)) → +(p1, +(p5, z0))
+(p5, p2) → +(p2, p5)
+(p5, +(p2, z0)) → +(p2, +(p5, z0))
+(p5, +(p5, z0)) → +(p10, z0)
+(p10, p1) → +(p1, p10)
+(p10, +(p1, z0)) → +(p1, +(p10, z0))
+(p10, p2) → +(p2, p10)
+(p10, +(p2, z0)) → +(p2, +(p10, z0))
+(p10, p5) → +(p5, p10)
+(p10, +(p5, z0)) → +(p5, +(p10, z0))
Tuples:

+'(+(z0, z1), z2) → c3(+'(z0, +(z1, z2)), +'(z1, z2))
+'(p1, +(p1, z0)) → c4(+'(p2, z0))
+'(p1, +(p2, +(p2, z0))) → c5(+'(p5, z0))
+'(p2, +(p1, z0)) → c7(+'(p1, +(p2, z0)), +'(p2, z0))
+'(p5, +(p5, z0)) → c14(+'(p10, z0))
+'(p10, +(p1, z0)) → c16(+'(p1, +(p10, z0)), +'(p10, z0))
+'(p10, +(p2, z0)) → c18(+'(p2, +(p10, z0)), +'(p10, z0))
+'(p10, +(p5, z0)) → c20(+'(p5, +(p10, z0)), +'(p10, z0))
+'(p2, +(p2, +(p2, +(p5, z0)))) → c9(+'(p1, +(p10, z0)), +'(p5, +(p5, z0)))
+'(p2, +(p2, +(p2, x0))) → c9(+'(p5, x0))
+'(p5, +(p1, +(p2, z0))) → c11(+'(p1, +(p2, +(p5, z0))), +'(p5, +(p2, z0)))
+'(p5, +(p1, +(p5, z0))) → c11(+'(p1, +(p10, z0)), +'(p5, +(p5, z0)))
+'(p5, +(p1, x0)) → c11(+'(p5, x0))
+'(p5, +(p2, +(p2, z0))) → c13(+'(p2, +(p2, +(p5, z0))), +'(p5, +(p2, z0)))
+'(p5, +(p2, +(p5, z0))) → c13(+'(p2, +(p10, z0)), +'(p5, +(p5, z0)))
+'(p5, +(p2, x0)) → c13(+'(p5, x0))
S tuples:

+'(p1, +(p1, z0)) → c4(+'(p2, z0))
+'(p1, +(p2, +(p2, z0))) → c5(+'(p5, z0))
+'(p2, +(p1, z0)) → c7(+'(p1, +(p2, z0)), +'(p2, z0))
+'(p5, +(p5, z0)) → c14(+'(p10, z0))
+'(p10, +(p1, z0)) → c16(+'(p1, +(p10, z0)), +'(p10, z0))
+'(p10, +(p2, z0)) → c18(+'(p2, +(p10, z0)), +'(p10, z0))
+'(p10, +(p5, z0)) → c20(+'(p5, +(p10, z0)), +'(p10, z0))
+'(p2, +(p2, +(p2, +(p5, z0)))) → c9(+'(p1, +(p10, z0)), +'(p5, +(p5, z0)))
+'(p2, +(p2, +(p2, x0))) → c9(+'(p5, x0))
+'(p5, +(p1, +(p2, z0))) → c11(+'(p1, +(p2, +(p5, z0))), +'(p5, +(p2, z0)))
+'(p5, +(p1, +(p5, z0))) → c11(+'(p1, +(p10, z0)), +'(p5, +(p5, z0)))
+'(p5, +(p1, x0)) → c11(+'(p5, x0))
+'(p5, +(p2, +(p2, z0))) → c13(+'(p2, +(p2, +(p5, z0))), +'(p5, +(p2, z0)))
+'(p5, +(p2, +(p5, z0))) → c13(+'(p2, +(p10, z0)), +'(p5, +(p5, z0)))
+'(p5, +(p2, x0)) → c13(+'(p5, x0))
K tuples:

+'(+(z0, z1), z2) → c3(+'(z0, +(z1, z2)), +'(z1, z2))
Defined Rule Symbols:

+

Defined Pair Symbols:

+'

Compound Symbols:

c3, c4, c5, c7, c14, c16, c18, c20, c9, c9, c11, c11, c13, c13

(19) CdtNarrowingProof (BOTH BOUNDS(ID, ID) transformation)

Use narrowing to replace +'(p10, +(p1, z0)) → c16(+'(p1, +(p10, z0)), +'(p10, z0)) by

+'(p10, +(p1, p2)) → c16(+'(p1, +(p2, p10)), +'(p10, p2))
+'(p10, +(p1, +(p2, z0))) → c16(+'(p1, +(p2, +(p10, z0))), +'(p10, +(p2, z0)))
+'(p10, +(p1, p5)) → c16(+'(p1, +(p5, p10)), +'(p10, p5))
+'(p10, +(p1, +(p5, z0))) → c16(+'(p1, +(p5, +(p10, z0))), +'(p10, +(p5, z0)))
+'(p10, +(p1, x0)) → c16(+'(p10, x0))

(20) Obligation:

Complexity Dependency Tuples Problem
Rules:

+(p1, p1) → p2
+(p1, +(p2, p2)) → p5
+(p5, p5) → p10
+(+(z0, z1), z2) → +(z0, +(z1, z2))
+(p1, +(p1, z0)) → +(p2, z0)
+(p1, +(p2, +(p2, z0))) → +(p5, z0)
+(p2, p1) → +(p1, p2)
+(p2, +(p1, z0)) → +(p1, +(p2, z0))
+(p2, +(p2, p2)) → +(p1, p5)
+(p2, +(p2, +(p2, z0))) → +(p1, +(p5, z0))
+(p5, p1) → +(p1, p5)
+(p5, +(p1, z0)) → +(p1, +(p5, z0))
+(p5, p2) → +(p2, p5)
+(p5, +(p2, z0)) → +(p2, +(p5, z0))
+(p5, +(p5, z0)) → +(p10, z0)
+(p10, p1) → +(p1, p10)
+(p10, +(p1, z0)) → +(p1, +(p10, z0))
+(p10, p2) → +(p2, p10)
+(p10, +(p2, z0)) → +(p2, +(p10, z0))
+(p10, p5) → +(p5, p10)
+(p10, +(p5, z0)) → +(p5, +(p10, z0))
Tuples:

+'(+(z0, z1), z2) → c3(+'(z0, +(z1, z2)), +'(z1, z2))
+'(p1, +(p1, z0)) → c4(+'(p2, z0))
+'(p1, +(p2, +(p2, z0))) → c5(+'(p5, z0))
+'(p2, +(p1, z0)) → c7(+'(p1, +(p2, z0)), +'(p2, z0))
+'(p5, +(p5, z0)) → c14(+'(p10, z0))
+'(p10, +(p2, z0)) → c18(+'(p2, +(p10, z0)), +'(p10, z0))
+'(p10, +(p5, z0)) → c20(+'(p5, +(p10, z0)), +'(p10, z0))
+'(p2, +(p2, +(p2, +(p5, z0)))) → c9(+'(p1, +(p10, z0)), +'(p5, +(p5, z0)))
+'(p2, +(p2, +(p2, x0))) → c9(+'(p5, x0))
+'(p5, +(p1, +(p2, z0))) → c11(+'(p1, +(p2, +(p5, z0))), +'(p5, +(p2, z0)))
+'(p5, +(p1, +(p5, z0))) → c11(+'(p1, +(p10, z0)), +'(p5, +(p5, z0)))
+'(p5, +(p1, x0)) → c11(+'(p5, x0))
+'(p5, +(p2, +(p2, z0))) → c13(+'(p2, +(p2, +(p5, z0))), +'(p5, +(p2, z0)))
+'(p5, +(p2, +(p5, z0))) → c13(+'(p2, +(p10, z0)), +'(p5, +(p5, z0)))
+'(p5, +(p2, x0)) → c13(+'(p5, x0))
+'(p10, +(p1, p2)) → c16(+'(p1, +(p2, p10)), +'(p10, p2))
+'(p10, +(p1, +(p2, z0))) → c16(+'(p1, +(p2, +(p10, z0))), +'(p10, +(p2, z0)))
+'(p10, +(p1, p5)) → c16(+'(p1, +(p5, p10)), +'(p10, p5))
+'(p10, +(p1, +(p5, z0))) → c16(+'(p1, +(p5, +(p10, z0))), +'(p10, +(p5, z0)))
+'(p10, +(p1, x0)) → c16(+'(p10, x0))
S tuples:

+'(p1, +(p1, z0)) → c4(+'(p2, z0))
+'(p1, +(p2, +(p2, z0))) → c5(+'(p5, z0))
+'(p2, +(p1, z0)) → c7(+'(p1, +(p2, z0)), +'(p2, z0))
+'(p5, +(p5, z0)) → c14(+'(p10, z0))
+'(p10, +(p2, z0)) → c18(+'(p2, +(p10, z0)), +'(p10, z0))
+'(p10, +(p5, z0)) → c20(+'(p5, +(p10, z0)), +'(p10, z0))
+'(p2, +(p2, +(p2, +(p5, z0)))) → c9(+'(p1, +(p10, z0)), +'(p5, +(p5, z0)))
+'(p2, +(p2, +(p2, x0))) → c9(+'(p5, x0))
+'(p5, +(p1, +(p2, z0))) → c11(+'(p1, +(p2, +(p5, z0))), +'(p5, +(p2, z0)))
+'(p5, +(p1, +(p5, z0))) → c11(+'(p1, +(p10, z0)), +'(p5, +(p5, z0)))
+'(p5, +(p1, x0)) → c11(+'(p5, x0))
+'(p5, +(p2, +(p2, z0))) → c13(+'(p2, +(p2, +(p5, z0))), +'(p5, +(p2, z0)))
+'(p5, +(p2, +(p5, z0))) → c13(+'(p2, +(p10, z0)), +'(p5, +(p5, z0)))
+'(p5, +(p2, x0)) → c13(+'(p5, x0))
+'(p10, +(p1, p2)) → c16(+'(p1, +(p2, p10)), +'(p10, p2))
+'(p10, +(p1, +(p2, z0))) → c16(+'(p1, +(p2, +(p10, z0))), +'(p10, +(p2, z0)))
+'(p10, +(p1, p5)) → c16(+'(p1, +(p5, p10)), +'(p10, p5))
+'(p10, +(p1, +(p5, z0))) → c16(+'(p1, +(p5, +(p10, z0))), +'(p10, +(p5, z0)))
+'(p10, +(p1, x0)) → c16(+'(p10, x0))
K tuples:

+'(+(z0, z1), z2) → c3(+'(z0, +(z1, z2)), +'(z1, z2))
Defined Rule Symbols:

+

Defined Pair Symbols:

+'

Compound Symbols:

c3, c4, c5, c7, c14, c18, c20, c9, c9, c11, c11, c13, c13, c16, c16

(21) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID) transformation)

Removed 2 trailing nodes:

+'(p10, +(p1, p5)) → c16(+'(p1, +(p5, p10)), +'(p10, p5))
+'(p10, +(p1, p2)) → c16(+'(p1, +(p2, p10)), +'(p10, p2))

(22) Obligation:

Complexity Dependency Tuples Problem
Rules:

+(p1, p1) → p2
+(p1, +(p2, p2)) → p5
+(p5, p5) → p10
+(+(z0, z1), z2) → +(z0, +(z1, z2))
+(p1, +(p1, z0)) → +(p2, z0)
+(p1, +(p2, +(p2, z0))) → +(p5, z0)
+(p2, p1) → +(p1, p2)
+(p2, +(p1, z0)) → +(p1, +(p2, z0))
+(p2, +(p2, p2)) → +(p1, p5)
+(p2, +(p2, +(p2, z0))) → +(p1, +(p5, z0))
+(p5, p1) → +(p1, p5)
+(p5, +(p1, z0)) → +(p1, +(p5, z0))
+(p5, p2) → +(p2, p5)
+(p5, +(p2, z0)) → +(p2, +(p5, z0))
+(p5, +(p5, z0)) → +(p10, z0)
+(p10, p1) → +(p1, p10)
+(p10, +(p1, z0)) → +(p1, +(p10, z0))
+(p10, p2) → +(p2, p10)
+(p10, +(p2, z0)) → +(p2, +(p10, z0))
+(p10, p5) → +(p5, p10)
+(p10, +(p5, z0)) → +(p5, +(p10, z0))
Tuples:

+'(+(z0, z1), z2) → c3(+'(z0, +(z1, z2)), +'(z1, z2))
+'(p1, +(p1, z0)) → c4(+'(p2, z0))
+'(p1, +(p2, +(p2, z0))) → c5(+'(p5, z0))
+'(p2, +(p1, z0)) → c7(+'(p1, +(p2, z0)), +'(p2, z0))
+'(p5, +(p5, z0)) → c14(+'(p10, z0))
+'(p10, +(p2, z0)) → c18(+'(p2, +(p10, z0)), +'(p10, z0))
+'(p10, +(p5, z0)) → c20(+'(p5, +(p10, z0)), +'(p10, z0))
+'(p2, +(p2, +(p2, +(p5, z0)))) → c9(+'(p1, +(p10, z0)), +'(p5, +(p5, z0)))
+'(p2, +(p2, +(p2, x0))) → c9(+'(p5, x0))
+'(p5, +(p1, +(p2, z0))) → c11(+'(p1, +(p2, +(p5, z0))), +'(p5, +(p2, z0)))
+'(p5, +(p1, +(p5, z0))) → c11(+'(p1, +(p10, z0)), +'(p5, +(p5, z0)))
+'(p5, +(p1, x0)) → c11(+'(p5, x0))
+'(p5, +(p2, +(p2, z0))) → c13(+'(p2, +(p2, +(p5, z0))), +'(p5, +(p2, z0)))
+'(p5, +(p2, +(p5, z0))) → c13(+'(p2, +(p10, z0)), +'(p5, +(p5, z0)))
+'(p5, +(p2, x0)) → c13(+'(p5, x0))
+'(p10, +(p1, +(p2, z0))) → c16(+'(p1, +(p2, +(p10, z0))), +'(p10, +(p2, z0)))
+'(p10, +(p1, +(p5, z0))) → c16(+'(p1, +(p5, +(p10, z0))), +'(p10, +(p5, z0)))
+'(p10, +(p1, x0)) → c16(+'(p10, x0))
S tuples:

+'(p1, +(p1, z0)) → c4(+'(p2, z0))
+'(p1, +(p2, +(p2, z0))) → c5(+'(p5, z0))
+'(p2, +(p1, z0)) → c7(+'(p1, +(p2, z0)), +'(p2, z0))
+'(p5, +(p5, z0)) → c14(+'(p10, z0))
+'(p10, +(p2, z0)) → c18(+'(p2, +(p10, z0)), +'(p10, z0))
+'(p10, +(p5, z0)) → c20(+'(p5, +(p10, z0)), +'(p10, z0))
+'(p2, +(p2, +(p2, +(p5, z0)))) → c9(+'(p1, +(p10, z0)), +'(p5, +(p5, z0)))
+'(p2, +(p2, +(p2, x0))) → c9(+'(p5, x0))
+'(p5, +(p1, +(p2, z0))) → c11(+'(p1, +(p2, +(p5, z0))), +'(p5, +(p2, z0)))
+'(p5, +(p1, +(p5, z0))) → c11(+'(p1, +(p10, z0)), +'(p5, +(p5, z0)))
+'(p5, +(p1, x0)) → c11(+'(p5, x0))
+'(p5, +(p2, +(p2, z0))) → c13(+'(p2, +(p2, +(p5, z0))), +'(p5, +(p2, z0)))
+'(p5, +(p2, +(p5, z0))) → c13(+'(p2, +(p10, z0)), +'(p5, +(p5, z0)))
+'(p5, +(p2, x0)) → c13(+'(p5, x0))
+'(p10, +(p1, +(p2, z0))) → c16(+'(p1, +(p2, +(p10, z0))), +'(p10, +(p2, z0)))
+'(p10, +(p1, +(p5, z0))) → c16(+'(p1, +(p5, +(p10, z0))), +'(p10, +(p5, z0)))
+'(p10, +(p1, x0)) → c16(+'(p10, x0))
K tuples:

+'(+(z0, z1), z2) → c3(+'(z0, +(z1, z2)), +'(z1, z2))
Defined Rule Symbols:

+

Defined Pair Symbols:

+'

Compound Symbols:

c3, c4, c5, c7, c14, c18, c20, c9, c9, c11, c11, c13, c13, c16, c16

(23) CdtNarrowingProof (BOTH BOUNDS(ID, ID) transformation)

Use narrowing to replace +'(p10, +(p2, z0)) → c18(+'(p2, +(p10, z0)), +'(p10, z0)) by

+'(p10, +(p2, p2)) → c18(+'(p2, +(p2, p10)), +'(p10, p2))
+'(p10, +(p2, +(p2, z0))) → c18(+'(p2, +(p2, +(p10, z0))), +'(p10, +(p2, z0)))
+'(p10, +(p2, p5)) → c18(+'(p2, +(p5, p10)), +'(p10, p5))
+'(p10, +(p2, +(p5, z0))) → c18(+'(p2, +(p5, +(p10, z0))), +'(p10, +(p5, z0)))
+'(p10, +(p2, x0)) → c18(+'(p10, x0))

(24) Obligation:

Complexity Dependency Tuples Problem
Rules:

+(p1, p1) → p2
+(p1, +(p2, p2)) → p5
+(p5, p5) → p10
+(+(z0, z1), z2) → +(z0, +(z1, z2))
+(p1, +(p1, z0)) → +(p2, z0)
+(p1, +(p2, +(p2, z0))) → +(p5, z0)
+(p2, p1) → +(p1, p2)
+(p2, +(p1, z0)) → +(p1, +(p2, z0))
+(p2, +(p2, p2)) → +(p1, p5)
+(p2, +(p2, +(p2, z0))) → +(p1, +(p5, z0))
+(p5, p1) → +(p1, p5)
+(p5, +(p1, z0)) → +(p1, +(p5, z0))
+(p5, p2) → +(p2, p5)
+(p5, +(p2, z0)) → +(p2, +(p5, z0))
+(p5, +(p5, z0)) → +(p10, z0)
+(p10, p1) → +(p1, p10)
+(p10, +(p1, z0)) → +(p1, +(p10, z0))
+(p10, p2) → +(p2, p10)
+(p10, +(p2, z0)) → +(p2, +(p10, z0))
+(p10, p5) → +(p5, p10)
+(p10, +(p5, z0)) → +(p5, +(p10, z0))
Tuples:

+'(+(z0, z1), z2) → c3(+'(z0, +(z1, z2)), +'(z1, z2))
+'(p1, +(p1, z0)) → c4(+'(p2, z0))
+'(p1, +(p2, +(p2, z0))) → c5(+'(p5, z0))
+'(p2, +(p1, z0)) → c7(+'(p1, +(p2, z0)), +'(p2, z0))
+'(p5, +(p5, z0)) → c14(+'(p10, z0))
+'(p10, +(p5, z0)) → c20(+'(p5, +(p10, z0)), +'(p10, z0))
+'(p2, +(p2, +(p2, +(p5, z0)))) → c9(+'(p1, +(p10, z0)), +'(p5, +(p5, z0)))
+'(p2, +(p2, +(p2, x0))) → c9(+'(p5, x0))
+'(p5, +(p1, +(p2, z0))) → c11(+'(p1, +(p2, +(p5, z0))), +'(p5, +(p2, z0)))
+'(p5, +(p1, +(p5, z0))) → c11(+'(p1, +(p10, z0)), +'(p5, +(p5, z0)))
+'(p5, +(p1, x0)) → c11(+'(p5, x0))
+'(p5, +(p2, +(p2, z0))) → c13(+'(p2, +(p2, +(p5, z0))), +'(p5, +(p2, z0)))
+'(p5, +(p2, +(p5, z0))) → c13(+'(p2, +(p10, z0)), +'(p5, +(p5, z0)))
+'(p5, +(p2, x0)) → c13(+'(p5, x0))
+'(p10, +(p1, +(p2, z0))) → c16(+'(p1, +(p2, +(p10, z0))), +'(p10, +(p2, z0)))
+'(p10, +(p1, +(p5, z0))) → c16(+'(p1, +(p5, +(p10, z0))), +'(p10, +(p5, z0)))
+'(p10, +(p1, x0)) → c16(+'(p10, x0))
+'(p10, +(p2, p2)) → c18(+'(p2, +(p2, p10)), +'(p10, p2))
+'(p10, +(p2, +(p2, z0))) → c18(+'(p2, +(p2, +(p10, z0))), +'(p10, +(p2, z0)))
+'(p10, +(p2, p5)) → c18(+'(p2, +(p5, p10)), +'(p10, p5))
+'(p10, +(p2, +(p5, z0))) → c18(+'(p2, +(p5, +(p10, z0))), +'(p10, +(p5, z0)))
+'(p10, +(p2, x0)) → c18(+'(p10, x0))
S tuples:

+'(p1, +(p1, z0)) → c4(+'(p2, z0))
+'(p1, +(p2, +(p2, z0))) → c5(+'(p5, z0))
+'(p2, +(p1, z0)) → c7(+'(p1, +(p2, z0)), +'(p2, z0))
+'(p5, +(p5, z0)) → c14(+'(p10, z0))
+'(p10, +(p5, z0)) → c20(+'(p5, +(p10, z0)), +'(p10, z0))
+'(p2, +(p2, +(p2, +(p5, z0)))) → c9(+'(p1, +(p10, z0)), +'(p5, +(p5, z0)))
+'(p2, +(p2, +(p2, x0))) → c9(+'(p5, x0))
+'(p5, +(p1, +(p2, z0))) → c11(+'(p1, +(p2, +(p5, z0))), +'(p5, +(p2, z0)))
+'(p5, +(p1, +(p5, z0))) → c11(+'(p1, +(p10, z0)), +'(p5, +(p5, z0)))
+'(p5, +(p1, x0)) → c11(+'(p5, x0))
+'(p5, +(p2, +(p2, z0))) → c13(+'(p2, +(p2, +(p5, z0))), +'(p5, +(p2, z0)))
+'(p5, +(p2, +(p5, z0))) → c13(+'(p2, +(p10, z0)), +'(p5, +(p5, z0)))
+'(p5, +(p2, x0)) → c13(+'(p5, x0))
+'(p10, +(p1, +(p2, z0))) → c16(+'(p1, +(p2, +(p10, z0))), +'(p10, +(p2, z0)))
+'(p10, +(p1, +(p5, z0))) → c16(+'(p1, +(p5, +(p10, z0))), +'(p10, +(p5, z0)))
+'(p10, +(p1, x0)) → c16(+'(p10, x0))
+'(p10, +(p2, p2)) → c18(+'(p2, +(p2, p10)), +'(p10, p2))
+'(p10, +(p2, +(p2, z0))) → c18(+'(p2, +(p2, +(p10, z0))), +'(p10, +(p2, z0)))
+'(p10, +(p2, p5)) → c18(+'(p2, +(p5, p10)), +'(p10, p5))
+'(p10, +(p2, +(p5, z0))) → c18(+'(p2, +(p5, +(p10, z0))), +'(p10, +(p5, z0)))
+'(p10, +(p2, x0)) → c18(+'(p10, x0))
K tuples:

+'(+(z0, z1), z2) → c3(+'(z0, +(z1, z2)), +'(z1, z2))
Defined Rule Symbols:

+

Defined Pair Symbols:

+'

Compound Symbols:

c3, c4, c5, c7, c14, c20, c9, c9, c11, c11, c13, c13, c16, c16, c18, c18

(25) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID) transformation)

Removed 2 trailing nodes:

+'(p10, +(p2, p2)) → c18(+'(p2, +(p2, p10)), +'(p10, p2))
+'(p10, +(p2, p5)) → c18(+'(p2, +(p5, p10)), +'(p10, p5))

(26) Obligation:

Complexity Dependency Tuples Problem
Rules:

+(p1, p1) → p2
+(p1, +(p2, p2)) → p5
+(p5, p5) → p10
+(+(z0, z1), z2) → +(z0, +(z1, z2))
+(p1, +(p1, z0)) → +(p2, z0)
+(p1, +(p2, +(p2, z0))) → +(p5, z0)
+(p2, p1) → +(p1, p2)
+(p2, +(p1, z0)) → +(p1, +(p2, z0))
+(p2, +(p2, p2)) → +(p1, p5)
+(p2, +(p2, +(p2, z0))) → +(p1, +(p5, z0))
+(p5, p1) → +(p1, p5)
+(p5, +(p1, z0)) → +(p1, +(p5, z0))
+(p5, p2) → +(p2, p5)
+(p5, +(p2, z0)) → +(p2, +(p5, z0))
+(p5, +(p5, z0)) → +(p10, z0)
+(p10, p1) → +(p1, p10)
+(p10, +(p1, z0)) → +(p1, +(p10, z0))
+(p10, p2) → +(p2, p10)
+(p10, +(p2, z0)) → +(p2, +(p10, z0))
+(p10, p5) → +(p5, p10)
+(p10, +(p5, z0)) → +(p5, +(p10, z0))
Tuples:

+'(+(z0, z1), z2) → c3(+'(z0, +(z1, z2)), +'(z1, z2))
+'(p1, +(p1, z0)) → c4(+'(p2, z0))
+'(p1, +(p2, +(p2, z0))) → c5(+'(p5, z0))
+'(p2, +(p1, z0)) → c7(+'(p1, +(p2, z0)), +'(p2, z0))
+'(p5, +(p5, z0)) → c14(+'(p10, z0))
+'(p10, +(p5, z0)) → c20(+'(p5, +(p10, z0)), +'(p10, z0))
+'(p2, +(p2, +(p2, +(p5, z0)))) → c9(+'(p1, +(p10, z0)), +'(p5, +(p5, z0)))
+'(p2, +(p2, +(p2, x0))) → c9(+'(p5, x0))
+'(p5, +(p1, +(p2, z0))) → c11(+'(p1, +(p2, +(p5, z0))), +'(p5, +(p2, z0)))
+'(p5, +(p1, +(p5, z0))) → c11(+'(p1, +(p10, z0)), +'(p5, +(p5, z0)))
+'(p5, +(p1, x0)) → c11(+'(p5, x0))
+'(p5, +(p2, +(p2, z0))) → c13(+'(p2, +(p2, +(p5, z0))), +'(p5, +(p2, z0)))
+'(p5, +(p2, +(p5, z0))) → c13(+'(p2, +(p10, z0)), +'(p5, +(p5, z0)))
+'(p5, +(p2, x0)) → c13(+'(p5, x0))
+'(p10, +(p1, +(p2, z0))) → c16(+'(p1, +(p2, +(p10, z0))), +'(p10, +(p2, z0)))
+'(p10, +(p1, +(p5, z0))) → c16(+'(p1, +(p5, +(p10, z0))), +'(p10, +(p5, z0)))
+'(p10, +(p1, x0)) → c16(+'(p10, x0))
+'(p10, +(p2, +(p2, z0))) → c18(+'(p2, +(p2, +(p10, z0))), +'(p10, +(p2, z0)))
+'(p10, +(p2, +(p5, z0))) → c18(+'(p2, +(p5, +(p10, z0))), +'(p10, +(p5, z0)))
+'(p10, +(p2, x0)) → c18(+'(p10, x0))
S tuples:

+'(p1, +(p1, z0)) → c4(+'(p2, z0))
+'(p1, +(p2, +(p2, z0))) → c5(+'(p5, z0))
+'(p2, +(p1, z0)) → c7(+'(p1, +(p2, z0)), +'(p2, z0))
+'(p5, +(p5, z0)) → c14(+'(p10, z0))
+'(p10, +(p5, z0)) → c20(+'(p5, +(p10, z0)), +'(p10, z0))
+'(p2, +(p2, +(p2, +(p5, z0)))) → c9(+'(p1, +(p10, z0)), +'(p5, +(p5, z0)))
+'(p2, +(p2, +(p2, x0))) → c9(+'(p5, x0))
+'(p5, +(p1, +(p2, z0))) → c11(+'(p1, +(p2, +(p5, z0))), +'(p5, +(p2, z0)))
+'(p5, +(p1, +(p5, z0))) → c11(+'(p1, +(p10, z0)), +'(p5, +(p5, z0)))
+'(p5, +(p1, x0)) → c11(+'(p5, x0))
+'(p5, +(p2, +(p2, z0))) → c13(+'(p2, +(p2, +(p5, z0))), +'(p5, +(p2, z0)))
+'(p5, +(p2, +(p5, z0))) → c13(+'(p2, +(p10, z0)), +'(p5, +(p5, z0)))
+'(p5, +(p2, x0)) → c13(+'(p5, x0))
+'(p10, +(p1, +(p2, z0))) → c16(+'(p1, +(p2, +(p10, z0))), +'(p10, +(p2, z0)))
+'(p10, +(p1, +(p5, z0))) → c16(+'(p1, +(p5, +(p10, z0))), +'(p10, +(p5, z0)))
+'(p10, +(p1, x0)) → c16(+'(p10, x0))
+'(p10, +(p2, +(p2, z0))) → c18(+'(p2, +(p2, +(p10, z0))), +'(p10, +(p2, z0)))
+'(p10, +(p2, +(p5, z0))) → c18(+'(p2, +(p5, +(p10, z0))), +'(p10, +(p5, z0)))
+'(p10, +(p2, x0)) → c18(+'(p10, x0))
K tuples:

+'(+(z0, z1), z2) → c3(+'(z0, +(z1, z2)), +'(z1, z2))
Defined Rule Symbols:

+

Defined Pair Symbols:

+'

Compound Symbols:

c3, c4, c5, c7, c14, c20, c9, c9, c11, c11, c13, c13, c16, c16, c18, c18

(27) CdtNarrowingProof (BOTH BOUNDS(ID, ID) transformation)

Use narrowing to replace +'(p10, +(p5, z0)) → c20(+'(p5, +(p10, z0)), +'(p10, z0)) by

+'(p10, +(p5, x0)) → c20(+'(p10, x0))

(28) Obligation:

Complexity Dependency Tuples Problem
Rules:

+(p1, p1) → p2
+(p1, +(p2, p2)) → p5
+(p5, p5) → p10
+(+(z0, z1), z2) → +(z0, +(z1, z2))
+(p1, +(p1, z0)) → +(p2, z0)
+(p1, +(p2, +(p2, z0))) → +(p5, z0)
+(p2, p1) → +(p1, p2)
+(p2, +(p1, z0)) → +(p1, +(p2, z0))
+(p2, +(p2, p2)) → +(p1, p5)
+(p2, +(p2, +(p2, z0))) → +(p1, +(p5, z0))
+(p5, p1) → +(p1, p5)
+(p5, +(p1, z0)) → +(p1, +(p5, z0))
+(p5, p2) → +(p2, p5)
+(p5, +(p2, z0)) → +(p2, +(p5, z0))
+(p5, +(p5, z0)) → +(p10, z0)
+(p10, p1) → +(p1, p10)
+(p10, +(p1, z0)) → +(p1, +(p10, z0))
+(p10, p2) → +(p2, p10)
+(p10, +(p2, z0)) → +(p2, +(p10, z0))
+(p10, p5) → +(p5, p10)
+(p10, +(p5, z0)) → +(p5, +(p10, z0))
Tuples:

+'(+(z0, z1), z2) → c3(+'(z0, +(z1, z2)), +'(z1, z2))
+'(p1, +(p1, z0)) → c4(+'(p2, z0))
+'(p1, +(p2, +(p2, z0))) → c5(+'(p5, z0))
+'(p2, +(p1, z0)) → c7(+'(p1, +(p2, z0)), +'(p2, z0))
+'(p5, +(p5, z0)) → c14(+'(p10, z0))
+'(p2, +(p2, +(p2, +(p5, z0)))) → c9(+'(p1, +(p10, z0)), +'(p5, +(p5, z0)))
+'(p2, +(p2, +(p2, x0))) → c9(+'(p5, x0))
+'(p5, +(p1, +(p2, z0))) → c11(+'(p1, +(p2, +(p5, z0))), +'(p5, +(p2, z0)))
+'(p5, +(p1, +(p5, z0))) → c11(+'(p1, +(p10, z0)), +'(p5, +(p5, z0)))
+'(p5, +(p1, x0)) → c11(+'(p5, x0))
+'(p5, +(p2, +(p2, z0))) → c13(+'(p2, +(p2, +(p5, z0))), +'(p5, +(p2, z0)))
+'(p5, +(p2, +(p5, z0))) → c13(+'(p2, +(p10, z0)), +'(p5, +(p5, z0)))
+'(p5, +(p2, x0)) → c13(+'(p5, x0))
+'(p10, +(p1, +(p2, z0))) → c16(+'(p1, +(p2, +(p10, z0))), +'(p10, +(p2, z0)))
+'(p10, +(p1, +(p5, z0))) → c16(+'(p1, +(p5, +(p10, z0))), +'(p10, +(p5, z0)))
+'(p10, +(p1, x0)) → c16(+'(p10, x0))
+'(p10, +(p2, +(p2, z0))) → c18(+'(p2, +(p2, +(p10, z0))), +'(p10, +(p2, z0)))
+'(p10, +(p2, +(p5, z0))) → c18(+'(p2, +(p5, +(p10, z0))), +'(p10, +(p5, z0)))
+'(p10, +(p2, x0)) → c18(+'(p10, x0))
+'(p10, +(p5, x0)) → c20(+'(p10, x0))
S tuples:

+'(p1, +(p1, z0)) → c4(+'(p2, z0))
+'(p1, +(p2, +(p2, z0))) → c5(+'(p5, z0))
+'(p2, +(p1, z0)) → c7(+'(p1, +(p2, z0)), +'(p2, z0))
+'(p5, +(p5, z0)) → c14(+'(p10, z0))
+'(p2, +(p2, +(p2, +(p5, z0)))) → c9(+'(p1, +(p10, z0)), +'(p5, +(p5, z0)))
+'(p2, +(p2, +(p2, x0))) → c9(+'(p5, x0))
+'(p5, +(p1, +(p2, z0))) → c11(+'(p1, +(p2, +(p5, z0))), +'(p5, +(p2, z0)))
+'(p5, +(p1, +(p5, z0))) → c11(+'(p1, +(p10, z0)), +'(p5, +(p5, z0)))
+'(p5, +(p1, x0)) → c11(+'(p5, x0))
+'(p5, +(p2, +(p2, z0))) → c13(+'(p2, +(p2, +(p5, z0))), +'(p5, +(p2, z0)))
+'(p5, +(p2, +(p5, z0))) → c13(+'(p2, +(p10, z0)), +'(p5, +(p5, z0)))
+'(p5, +(p2, x0)) → c13(+'(p5, x0))
+'(p10, +(p1, +(p2, z0))) → c16(+'(p1, +(p2, +(p10, z0))), +'(p10, +(p2, z0)))
+'(p10, +(p1, +(p5, z0))) → c16(+'(p1, +(p5, +(p10, z0))), +'(p10, +(p5, z0)))
+'(p10, +(p1, x0)) → c16(+'(p10, x0))
+'(p10, +(p2, +(p2, z0))) → c18(+'(p2, +(p2, +(p10, z0))), +'(p10, +(p2, z0)))
+'(p10, +(p2, +(p5, z0))) → c18(+'(p2, +(p5, +(p10, z0))), +'(p10, +(p5, z0)))
+'(p10, +(p2, x0)) → c18(+'(p10, x0))
+'(p10, +(p5, x0)) → c20(+'(p10, x0))
K tuples:

+'(+(z0, z1), z2) → c3(+'(z0, +(z1, z2)), +'(z1, z2))
Defined Rule Symbols:

+

Defined Pair Symbols:

+'

Compound Symbols:

c3, c4, c5, c7, c14, c9, c9, c11, c11, c13, c13, c16, c16, c18, c18, c20

(29) CdtNarrowingProof (BOTH BOUNDS(ID, ID) transformation)

Use narrowing to replace +'(p2, +(p2, +(p2, +(p5, z0)))) → c9(+'(p1, +(p10, z0)), +'(p5, +(p5, z0))) by

+'(p2, +(p2, +(p2, +(p5, x0)))) → c9(+'(p5, +(p5, x0)))

(30) Obligation:

Complexity Dependency Tuples Problem
Rules:

+(p1, p1) → p2
+(p1, +(p2, p2)) → p5
+(p5, p5) → p10
+(+(z0, z1), z2) → +(z0, +(z1, z2))
+(p1, +(p1, z0)) → +(p2, z0)
+(p1, +(p2, +(p2, z0))) → +(p5, z0)
+(p2, p1) → +(p1, p2)
+(p2, +(p1, z0)) → +(p1, +(p2, z0))
+(p2, +(p2, p2)) → +(p1, p5)
+(p2, +(p2, +(p2, z0))) → +(p1, +(p5, z0))
+(p5, p1) → +(p1, p5)
+(p5, +(p1, z0)) → +(p1, +(p5, z0))
+(p5, p2) → +(p2, p5)
+(p5, +(p2, z0)) → +(p2, +(p5, z0))
+(p5, +(p5, z0)) → +(p10, z0)
+(p10, p1) → +(p1, p10)
+(p10, +(p1, z0)) → +(p1, +(p10, z0))
+(p10, p2) → +(p2, p10)
+(p10, +(p2, z0)) → +(p2, +(p10, z0))
+(p10, p5) → +(p5, p10)
+(p10, +(p5, z0)) → +(p5, +(p10, z0))
Tuples:

+'(+(z0, z1), z2) → c3(+'(z0, +(z1, z2)), +'(z1, z2))
+'(p1, +(p1, z0)) → c4(+'(p2, z0))
+'(p1, +(p2, +(p2, z0))) → c5(+'(p5, z0))
+'(p2, +(p1, z0)) → c7(+'(p1, +(p2, z0)), +'(p2, z0))
+'(p5, +(p5, z0)) → c14(+'(p10, z0))
+'(p2, +(p2, +(p2, x0))) → c9(+'(p5, x0))
+'(p5, +(p1, +(p2, z0))) → c11(+'(p1, +(p2, +(p5, z0))), +'(p5, +(p2, z0)))
+'(p5, +(p1, +(p5, z0))) → c11(+'(p1, +(p10, z0)), +'(p5, +(p5, z0)))
+'(p5, +(p1, x0)) → c11(+'(p5, x0))
+'(p5, +(p2, +(p2, z0))) → c13(+'(p2, +(p2, +(p5, z0))), +'(p5, +(p2, z0)))
+'(p5, +(p2, +(p5, z0))) → c13(+'(p2, +(p10, z0)), +'(p5, +(p5, z0)))
+'(p5, +(p2, x0)) → c13(+'(p5, x0))
+'(p10, +(p1, +(p2, z0))) → c16(+'(p1, +(p2, +(p10, z0))), +'(p10, +(p2, z0)))
+'(p10, +(p1, +(p5, z0))) → c16(+'(p1, +(p5, +(p10, z0))), +'(p10, +(p5, z0)))
+'(p10, +(p1, x0)) → c16(+'(p10, x0))
+'(p10, +(p2, +(p2, z0))) → c18(+'(p2, +(p2, +(p10, z0))), +'(p10, +(p2, z0)))
+'(p10, +(p2, +(p5, z0))) → c18(+'(p2, +(p5, +(p10, z0))), +'(p10, +(p5, z0)))
+'(p10, +(p2, x0)) → c18(+'(p10, x0))
+'(p10, +(p5, x0)) → c20(+'(p10, x0))
+'(p2, +(p2, +(p2, +(p5, x0)))) → c9(+'(p5, +(p5, x0)))
S tuples:

+'(p1, +(p1, z0)) → c4(+'(p2, z0))
+'(p1, +(p2, +(p2, z0))) → c5(+'(p5, z0))
+'(p2, +(p1, z0)) → c7(+'(p1, +(p2, z0)), +'(p2, z0))
+'(p5, +(p5, z0)) → c14(+'(p10, z0))
+'(p2, +(p2, +(p2, x0))) → c9(+'(p5, x0))
+'(p5, +(p1, +(p2, z0))) → c11(+'(p1, +(p2, +(p5, z0))), +'(p5, +(p2, z0)))
+'(p5, +(p1, +(p5, z0))) → c11(+'(p1, +(p10, z0)), +'(p5, +(p5, z0)))
+'(p5, +(p1, x0)) → c11(+'(p5, x0))
+'(p5, +(p2, +(p2, z0))) → c13(+'(p2, +(p2, +(p5, z0))), +'(p5, +(p2, z0)))
+'(p5, +(p2, +(p5, z0))) → c13(+'(p2, +(p10, z0)), +'(p5, +(p5, z0)))
+'(p5, +(p2, x0)) → c13(+'(p5, x0))
+'(p10, +(p1, +(p2, z0))) → c16(+'(p1, +(p2, +(p10, z0))), +'(p10, +(p2, z0)))
+'(p10, +(p1, +(p5, z0))) → c16(+'(p1, +(p5, +(p10, z0))), +'(p10, +(p5, z0)))
+'(p10, +(p1, x0)) → c16(+'(p10, x0))
+'(p10, +(p2, +(p2, z0))) → c18(+'(p2, +(p2, +(p10, z0))), +'(p10, +(p2, z0)))
+'(p10, +(p2, +(p5, z0))) → c18(+'(p2, +(p5, +(p10, z0))), +'(p10, +(p5, z0)))
+'(p10, +(p2, x0)) → c18(+'(p10, x0))
+'(p10, +(p5, x0)) → c20(+'(p10, x0))
+'(p2, +(p2, +(p2, +(p5, x0)))) → c9(+'(p5, +(p5, x0)))
K tuples:

+'(+(z0, z1), z2) → c3(+'(z0, +(z1, z2)), +'(z1, z2))
Defined Rule Symbols:

+

Defined Pair Symbols:

+'

Compound Symbols:

c3, c4, c5, c7, c14, c9, c11, c11, c13, c13, c16, c16, c18, c18, c20

(31) CpxTrsMatchBoundsTAProof (EQUIVALENT transformation)

A linear upper bound on the runtime complexity of the TRS R could be shown with a Match-Bound[TAB_LEFTLINEAR,TAB_NONLEFTLINEAR] (for contructor-based start-terms) of 1.

The compatible tree automaton used to show the Match-Boundedness (for constructor-based start-terms) is represented by:
final states : [1]
transitions:
p10() → 0
p20() → 0
p50() → 0
p100() → 0
+0(0, 0) → 1
p21() → 1
p101() → 1
p11() → 2
p21() → 3
+1(2, 3) → 1
p51() → 4
+1(2, 4) → 1
p21() → 5
+1(5, 4) → 1
p101() → 6
+1(2, 6) → 1
+1(5, 6) → 1
p51() → 7
+1(7, 6) → 1

(32) BOUNDS(O(1), O(n^1))